1. $T$ : Type
\\[0ex]2. $T$ List
\\[0ex]$\vdash$  $\forall$$n$:\{0$\ldots\,$0\}, $i$:\{0..(0 {-} $n$)$^{-}$\}. nth\_tl($n$;[])[$i$] = [][($i$+$n$)]